#!/bin/bash
Z3=/nethome/bmikek3/z3/build/z3
BOOLECTOR=/nethome/bmikek3/boolector/build/bin/boolector
CVC5=/nethome/bmikek3/cvc5/build/bin/cvc5

TIMEOUT=300
MEMORY_LIMIT=10000

FILE=$1


SLOT_OUT=$( { /usr/bin/time -f "tmr%e" timeout $TIMEOUT ./main-alo -r 5,11 -s $FILE -o $FILE-alo.smt2 -t fp-alo-stats.csv; } 2>&1 > /dev/null )
if [[ $? == 124 ]]
then
    SLOT_GOOD=false
    SLOT_TIME=$TIMEOUT
else
    SLOT_TIME=$(echo "$SLOT_OUT" | grep -Po 'tmr*.*' | tr -dc '.0-9')
fi

#sed -i '/declare-fun bvnego/d;/declare-fun bvsaddo/d;/declare-fun bvssubo/d;/declare-fun bvsmulo/d;/declare-fun bvsdivo/d' $FILE-aix-wnoc.smt2


#SLOT_OUT=$( { /usr/bin/time -f "tmr%e" timeout $TIMEOUT ./main -i aix -s $FILE -o $FILE-aix.smt2 -t lia-tool-stats.csv; } 2>&1 > /dev/null )
#if [[ $? == 124 ]]
#then
#    SLOT_GOOD=false
#    SLOT_TIME=$TIMEOUT
#else
#    SLOT_TIME=$(echo "$SLOT_OUT" | grep -Po 'tmr*.*' | tr -dc '.0-9')
#fi

#sed -i '/declare-fun bvnego/d;/declare-fun bvsaddo/d;/declare-fun bvssubo/d;/declare-fun bvsmulo/d;/declare-fun bvsdivo/d' $FILE-aix.smt2


#Z3----------------
#PRE_SOL_OUT=$( { /usr/bin/time -f "tmr%e" $Z3 $FILE -T:$TIMEOUT; } 2>&1 )
#if [[ "$PRE_SOL_OUT" == "timeout" ]]
#then
#    Z3_PRE_TIME=$TIMEOUT
#    Z3_PRE_RESULT="timeout"
#else
#    Z3_PRE_TIME=$(echo "$PRE_SOL_OUT" | grep -Po 'tmr*.*' | tr -dc '.0-9')
#    Z3_PRE_RESULT=$(echo $PRE_SOL_OUT | awk '{print $1;}')
#fi



#CV_OUT=$( { /usr/bin/time -f "tmr%e" $CVC5 $FILE -q  --tlimit=$(( 1000 * TIMEOUT )); } 2>&1 )
#if [[ "$CV_OUT" == *"timeout"* ]]
#then
#    CV_TIME=$TIMEOUT
#    CV_RESULT="timeout"
#else
#    CV_TIME=$(echo "$CV_OUT" | grep -Po 'tmr*.*' | tr -dc '.0-9')
#    CV_RESULT=$(echo $CV_OUT | awk '{print $1;}')
#fi


#echo "$FILE,$Z3_RESULT,$Z3_TIME,$CV_RESULT,$CV_TIME,$BL_RESULT,$BL_TIME"
echo "$FILE,$SLOT_TIME" >> fp-alo-times.csv